Nuprl Lemma : fpf-compatible-join2 11,40
A:Type, eq:EqDecider(A), B:(AType), f,g,h:fpf(A; a.B(a)).
fpf-compatible(A; a.B(a); eq; f; h)
 fpf-compatible(A; a.B(a); eq; g; h)
 fpf-compatible(A; a.B(a); eq; fpf-join(eq; f; g); h) 
latex

Definitionsx:A. B(x), x(s), P  Q, t  T, x. t(x), prop{i:l}
Lemmasfpf-compatible-symmetry, fpf-join wf, fpf-compatible-join, fpf-compatible wf, fpf wf, deq wf

origin